package ch.epfl.lara.matcheck.verify.provers;


/**
 * Possible results of a prover:
 *   - Valid  : Formula has been correctly checked
 *   - Timeout: A timeout has interrupted the check
 *   - Invalid: The formula is invalid
 */
object ProverResults  {
 
  abstract class ProverResult {
    def && (that: ProverResult): ProverResult = (this,that) match {
      case (a,b) if a == b => a
      case (a,b) if a == Invalid || b == Invalid => Invalid
      case (Valid,b) => b
      case (a,Valid) => a
    }
    
    def || (that: ProverResult): ProverResult = (this,that) match {
      case (a,b) if a == b => a
      case (a,b) if a == Valid || b == Valid => Valid
      case (Invalid,b) => b
      case (a,Invalid) => a
    }
  }
  final case object Valid extends ProverResult {
    override def toString: String = "valid"
  }
  final case object Timeout extends ProverResult {
    override def toString: String = "timeout"
  }
  final case object Invalid extends ProverResult {
    override def toString: String = "invalid"
  }
  
  /** negate the prover result */
  def neg(p: ProverResult): ProverResult = p match {
    case Valid   => Invalid
    case Invalid => Valid
    case Timeout => Timeout
  }
  
  
}
